perm filename RENEW.82[W82,JMC]1 blob sn#648966 filedate 1982-03-19 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	renew.82[w82,jmc]	1982 nsf renewal proposal
C00006 ENDMK
CāŠ—;
renew.82[w82,jmc]	1982 nsf renewal proposal
NSF (Y.T. Chien, Program Director, Intelligent Systems) wants it by
1982 April 15

	This is a request to continue for a second year the grant
MCS-8104877 (Basic Research in Artificial Intelligence).  During the
past year I made some progress on the following problems:

	1. Representation of facts about people's knowledge for use
in AI systems.  The main results concern the need to represent such
facts as

	a. All a person S knows about X is Y.  This is required if
one is to be able to conclude that he still won't know Z if he learns
W.  Delimiting knowledge is a problem that hasn't been attacked before
either in AI or in philosophy.

	b. A person knows about (say) oriental rugs.  This can be
said by a person who doesn't himself know about oriental rugs, so
he can't express it as an assertion that the expert knows some
particular facts.  Moreover, it needn't even be determined (whether
one knows it or not) what functions and predicates the expert uses
to express his knowledge.  Nevertheless, formalization of "knowing
about" is needed if AI programs are to decide to consult experts -
whether they be humans or other programs.

	Problem a is partially solved by going to second order logic
and writing



to mean


I don't yet know how to solve problem b.


	2. I have become interested in Kowalski's doctrine that

	progam = logic + control.

In order to make it work, some very powerful methods are needed
for expressing control.  The attached draft of a paper presented
at the Logic Programming Conference held at Long Beach describes
a map-coloring problem, a Prolog program giving its logic, and
the problem of expressing certain "postponement heuristics" as
control applied to that logic.  Prolog has turned out to be a
good vehicle for thinking about such problems.

	3. I have recently developed a first order theory of
what I call "dirty Lisp" programs, i.e. those involving imbedded SETQs,
RPLACA and RPLACD.  It looks like I can prove correctness of
such programs.  It involves the notion of the S-expression pointed
to by a location in a memory state.  Thus it turns out that the
theory of clean Lisp is an essential component of the theory of
dirty Lisp - not merely that the theory of dirty Lisp is a generalization
of the theory of clean Lisp, as I and others had previously thought.

	During the forthcoming year I expect to work on all these
problems.